COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Any pair of clauses has at most a finite number of resolvents because
C00005 00003	.SS(Completeness results,,R1:)
C00006 00004	.BEGIN "ATP"
C00009 00005
C00010 ENDMK
C⊗;
Any pair of clauses has at most a finite number of resolvents because
there are only finitely many pairs of sets of literals, ?L and ?M, and for
each pair, at most one substitution ?s0. The resolvents of a pair
of ground clauses are the ground resolvents. A resolution deduction is defined
as before with the more general resolvent taking the  
place of "ground resolvent".

There is a refutation of a set of clauses ?S (i.e. ?S%5*b%1)
iff %5b%1ε%6R%8n%1(?S)  for some n. Where 
%6R%8n%1 is defined on {yon(P100)} omitting the adjective "ground".
We can no longer be assured that the process of taking resolvents will ever 
"close#out", however, as we now have an infinite number of possible instances
of literals  any time our Herbrand domain contains a single constant and a single
function letter. Herbrand's theorem assures us that given an inconsistent
set of clauses ?S, some finite subset of ?H(?S) is inconsistent, thus
%5b%1ε%6R%8n%1(?S) for some n, but we cannot put a bound on that n. We have
no idea how long the program must run to establish the inconsistency of ?S
even though  we know that given enough time it will in fact do so.
The  problem arises when ?S is consistent; our process of taking resolvents
may close out, %2or%* it may keep running. Thus we do not have a decision
procedure for determining whether %5b%1ε?RN for any n, for an arbitrary set 
of clauses⊗↓A priori, this does not say that a general decision procedure
for proof does %2not%* exist; however a corollary of our future
undecidability of elementary number theory will indeed establish this.←.

.SS(Completeness results,,R1:)
.BEGIN NOFILL;group;

%7THEOREM 6%* Every theorem of predicate calculus is logically valid.
.BEGIN INDENT 10,10;fill;
By property 6) of the notion of truth ({yon(P13)}) axioms %7AX 1-3%1 are
logically valid. By property 7) corollary and property 8), %7AX 4%* and 
%7AX 5%1 are logically valid. By 2) and 5), the rules of inference
preserve logical validity. Thus, every theorem of predicate calculus is
logically valid.
.end
.end
.BEGIN "ATP"
.at "?P"⊂"%6P%1"⊃
.at "?R"⊂"%6R%1"⊃

.BEGIN NOFILL;
.BEGIN fill;
.group
%7LEMMA 7%1 If ?P⊂?H then ?R(?P(?S))⊂?P(?R(?S))

Proof: Suppose ?Cε?P(?S), then since ?S⊂?R(?S), ?Cε?P(?R(?S)).
.apart

If ?C is a resolvent, then ?C = (?A%ga%1-%dL%ga%1)∪(?B%gb%1-%dM%gb%1)
where ?A, ?Bε?S, ?A%ga%1, ?B%gb%1ε?P(?S), and %dL%ga%1 and %dM%gb%1 are
complemenatry literals.
.begin center;
Let %ga%1 = [(?s1, ?u1), ..., (?sk, ?uk)] and

%gb%1 = [(?t1, ?v1), ..., (?tm, ?vm)]
.end
where ?u1, ..., ?uk are all the variables in ?A
and ?v1,#...,#?vm are all the variables in ?B. 
Let  %gq%1#=[(%eu%4k+1%1,?v1),#...,#(%eu%4k+m%1,?vm)]
be the changes of
variables which standardize ?A and ?B apart, and let 

.begin center
%gs%1 =[(?s1, ?u1) ...(?sk, ?uk), (?tk, %eu%4k+1%1, ...(?tm, %eu%4k+m%1)].
.end

Then ?A%gs%1 = ?A%ga%1, ?B%gqs%1 = ?B%gb%1, and ?C = (?A-?L)%gs%1∪(?B-?M)%gqs%1.
where ?L%gs%1 = %dL%ga%1, and ?M%gqs%1 = %dM%gb%1. Furthermore, since %gs%1 unifies
the set ?L∪¬?M%gq%1 (where ¬?M%gq%1 is the set of negated literals of ?M%gq%1)
 there is a most general substitution ?s0
(chosen by previous algorithm)  and a resolvent ?C' of ?A and ?B, where
?C'#=#(?A-?L)?s0∪(?B-?M)?q?s0. Let %gs%*#=#?s0%gl%*; then ?C#=#?C'%gl%1.
Thus ?Cε?P(?R(?S)); that is, ?C is a substituton instance of a resolvent
of clauses in ?S.

The general form of lemma 7 follows by induction:
Assume ?R%8n%1(?P(?S))⊂?P(?RN); then:
.begin nofill;
		?R%8n+1%1(?P(?S))=?R(?R%8n%1(?P(?S)))
				⊂?R(?P(?RN))   by inductive assumption
				⊂?P(?R(?RN))   by lemma 7
				=?P(?R%8n+1%1(?S)) by definition

.end
.end
.end